/**
 * Copyright (c) 2010 by Kevin Bierhoff.
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *    1. Redistributions of source code must retain the above copyright
 *       notice, this list of conditions and the following disclaimer.
 *    2. Redistributions in binary form must reproduce the above copyright
 *       notice, this list of conditions and the following disclaimer in the
 *       documentation and/or other materials provided with the distribution.
 *    3. Neither the names of the authors nor the
 *       names of its contributors may be used to endorse or promote products
 *       derived from this software without specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE AUTHORS ''AS IS'' AND ANY
 * EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
 * WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
 * DISCLAIMED. IN NO EVENT SHALL THE AUTHORS BE LIABLE FOR ANY
 * DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
 * INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
 * LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND
 * ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
 * SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 */
package com.googlecode.syper.javasyp.prover;

import java.util.ArrayList;
import java.util.Collections;
import java.util.Deque;
import java.util.HashMap;
import java.util.LinkedHashMap;
import java.util.LinkedHashSet;
import java.util.LinkedList;
import java.util.List;
import java.util.Map;
import java.util.Set;
import java.util.Map.Entry;

import org.eclipse.jdt.core.dom.ITypeBinding;
import org.eclipse.jdt.core.dom.IVariableBinding;
import org.eclipse.jdt.core.dom.PrefixExpression;
import org.eclipse.jdt.core.dom.InfixExpression.Operator;

import com.googlecode.syper.javasyp.checker.RefType;
import com.googlecode.syper.javasyp.formulae.Field;
import com.googlecode.syper.javasyp.formulae.Formula;
import com.googlecode.syper.javasyp.formulae.FormulaVisitor;
import com.googlecode.syper.javasyp.formulae.Fun;
import com.googlecode.syper.javasyp.formulae.IfThenElse;
import com.googlecode.syper.javasyp.formulae.Infix;
import com.googlecode.syper.javasyp.formulae.Literal;
import com.googlecode.syper.javasyp.formulae.Local;
import com.googlecode.syper.javasyp.formulae.Name;
import com.googlecode.syper.javasyp.formulae.Pre;
import com.googlecode.syper.javasyp.formulae.Prefix;
import com.googlecode.syper.javasyp.formulae.Quantifier;
import com.googlecode.syper.javasyp.formulae.Select;
import com.googlecode.syper.javasyp.formulae.Store;

/**
 * @author kevin
 * @since Feb 8, 2010
 *
 */
class SmtLibFormatter extends FormulaVisitor<String> {

	/** Custom SMT sort for objects including arrays */
	public static final String OBJ_TYPE = "Obj";
	/** "Local" variables declared in quantifiers */
	private static final char SMT_VAR_PREFIX = '?';
	/** Maps Eclipse to SMT binary operators if direct mapping exists and unambiguous */
	private static final Map<Operator, String> BINOPS;

	static {
		Map<Operator, String> ops = new HashMap<Operator, String>();
		// comparison
		ops.put(Operator.EQUALS, "=");
		ops.put(Operator.GREATER, ">");
		ops.put(Operator.GREATER_EQUALS, ">=");
		ops.put(Operator.LEFT_SHIFT, ">");
		ops.put(Operator.LESS, "<");
		ops.put(Operator.LESS_EQUALS, "<=");
		// arithmetic (-+* work for ints and reals)
//		ops.put(Operator.DIVIDE, "/"); // need "div" if both args are ints
		ops.put(Operator.MINUS, "-");
		ops.put(Operator.PLUS, "+");
		ops.put(Operator.REMAINDER, "mod");
		ops.put(Operator.TIMES, "*");
		// bitshifting TODO these may not work (not part of Reals_Ints theory)
		ops.put(Operator.LEFT_SHIFT, "<<");
		ops.put(Operator.RIGHT_SHIFT_SIGNED, ">>");
		ops.put(Operator.RIGHT_SHIFT_UNSIGNED, ">>>");
		BINOPS = Collections.unmodifiableMap(ops);
	}

	/** maps variables to their SMT sorts */
	private final Map<String, String> variables =
		new LinkedHashMap<String, String>();

	/** maps fields (subset of {@link #variables}) to their binding */
	private final Map<String, IVariableBinding> fields =
		new LinkedHashMap<String, IVariableBinding>();

	/** string and character constants */
	private final Map<Object, String> constants =
		new LinkedHashMap<Object, String>();

	/** Field sorts and their incarnations */
	private final Set<HeapIncarnation> heaps = new LinkedHashSet<HeapIncarnation>();
	/** Array <b>element</b> sorts and their incarnations */
	private final Set<HeapIncarnation> arrays = new LinkedHashSet<HeapIncarnation>();
	/** stack of quantified variables */
	private final Deque<Local> quantified = new LinkedList<Local>();

	private final IFieldInfo checker;

	private boolean heapMapEncoding = false;
	private boolean useArrayStore = false;

	public SmtLibFormatter(IFieldInfo checker, boolean heapMapEncoding) {
		this.checker = checker;
		this.heapMapEncoding = heapMapEncoding;
	}

	@Override
	public String visit(Local f) {
		String id = getId(f);
		return id;
	}

	@Override
	public String visit(Field f) {
		if (heapMapEncoding) {
			String obj = f.getObj().dispatch(this);
			String sel = f.getSelector().dispatch(this);
			int incarnation = f.getIncarnation();
			String smtSort = getSort(f.getType());
			heaps.add(new HeapIncarnation(smtSort, incarnation));
			return "(deref" + smtSort + incarnation + " " + obj + " " + sel + ")";
		} else {
			String id = getId(f);
			return id;
		}
	}

	private String getId(Name n) {
		String id;
		assert n != null;
		if (n instanceof Local) {
			Local l = (Local) n;
			id = l.getId();
			// remove confusing stuff
			id = id.replace('(', '_').replace(')', '_').replace('/', '.').replace(';', '_');
			id = id.replace('$', '.').replace('~', '.'); // inner classes, top-level classes other than the one named like file
			id = id.replace('<', '\'').replace('>', '\'').replace(']', '\'').replace('[', '\'');
			if (quantified.contains(n))
				// do not populate variables map
				return SMT_VAR_PREFIX + id;
			if (l.isMeta()) {
				if (! heapMapEncoding)
					throw new IllegalStateException("Shouldn't see meta vars: " + l);
				if (! Local.FIELD_META_TYPE.equals(l.getMetaType()))
					throw new UnsupportedOperationException("Unknown meta type " + l.getMetaType() + " in " + l);
				String smtSort = getSort(l);
				variables.put(id, smtSort);
				fields.put(id, l.getBinding());
				return id;
			}
		} else if (heapMapEncoding) {
			throw new IllegalStateException("Shouldn't see fields: " + n);
		} else {
			Field f = (Field) n;
			id = getId((Name) f.getObj()) + '.' + f.getId();
		}
		variables.put(id, getSort(n.getType()));
		return id;
	}

	@Override
	public String visit(Infix f) {
		String op1 = f.getLhs().dispatch(this);
		String op = BINOPS.get(f.getOp());
		String op2 = f.getRhs().dispatch(this);
		if (op != null) {
			// nothing
		} else if (Operator.NOT_EQUALS.equals(f.getOp())) {
			return "(not (= " + op1 + " " + op2 + "))";
		} else if (Operator.DIVIDE.equals(f.getOp())) {
			// integer division is div but if a Real is involved must use /
			op = f.dispatch(Formula.IS_INTEGER) ? "div" : "/";
		} else if (f.isBoolean()) {
			if (Operator.AND.equals(f.getOp())) {
				op = "and";
			} else if (Operator.OR.equals(f.getOp())) {
				op = "or";
			} else if (Operator.XOR.equals(f.getOp())) {
				op = "xor";
			} else if (Operator.CONDITIONAL_AND.equals(f.getOp())) {
				op = "and";
//				op = "or";
//				op2 = "(and " + op1 + " " + op2 + ")";
//				op1 = "(not " + op1 + ")";
			} else if (Operator.CONDITIONAL_OR.equals(f.getOp())) {
				op = "or";
				op2 = "(and (not " + op1 + ") " + op2 + ")";
			} else {
				throw new IllegalArgumentException(f.toString());
			}
		} else {
			if (Operator.AND.equals(f.getOp())) {
				op = "&";
			} else if (Operator.OR.equals(f.getOp())) {
				op = "|";
			} else if (Operator.XOR.equals(f.getOp())) {
				op = "#";
			} else {
				throw new IllegalArgumentException(f.toString());
			}
		}
		return "(" + op + " " + op1 + " " + op2 + ")";
	}

	@Override
	public String visit(Literal f) {
		Object c = f.getValue();
		if (c == null || c instanceof Number || c instanceof Boolean)
			return String.valueOf(c);
		if (c instanceof Character)
			// encode characters with their integer value
			return String.valueOf(((int) ((Character) c).charValue()));
		// remember string constants
		String result = c instanceof ITypeBinding ?
				"type:" + ((ITypeBinding) c).getQualifiedName() : "str:" + String.valueOf(c);
		constants.put(c, result);
		return result;
	}

	@Override
	public String visit(Prefix f) {
		String operand = f.getRhs().dispatch(this);
		String op;
		if (PrefixExpression.Operator.COMPLEMENT.equals(f.getOp())) {
			op = "~";
		} else if (PrefixExpression.Operator.MINUS.equals(f.getOp())) {
			op = "-";
		} else if (PrefixExpression.Operator.NOT.equals(f.getOp())) {
			op = "not";
		} else if (PrefixExpression.Operator.PLUS.equals(f.getOp())) {
			return operand;
		} else {
			throw new IllegalArgumentException(f.toString());
		}
		return "(" + op + " " + operand + ")";
	}

	@Override
	public String visit(Select f) {
		String array = f.getArray().dispatch(this);
		String index = f.getIndex().dispatch(this);
		String sort = getSort(f.getType());
		int inc = f.getIncarnation();
		arrays.add(new HeapIncarnation(sort, inc));
		return "(select" + sort + inc + " " + array + " " + index + ")";
	}

	@Override
	public String visit(Store f) {
		if (! useArrayStore)
			throw new IllegalStateException("Shouldn't create: " + f);

		String array = f.getArray().dispatch(this);
		String index = f.getIndex().dispatch(this);
		String newVal = f.getNewValue().dispatch(this);
		String sort = getSort(f.getElementType());
		arrays.add(new HeapIncarnation(sort, 0 /* incarnations shouldn't be used */));
		return "(store" + sort + " " + array + " " + index + " " + newVal + ")";
	}

	@Override
	public String visit(Pre f) {
		throw new IllegalStateException("Not expected: " + f);
	}

	@Override
	public String visit(Quantifier f) {
		for (int i = 0; i < f.getVars().size(); ++i)
			quantified.push(f.getVars().get(i));
		try {
			String body = f.getBody().dispatch(this);
			String q = f.isExists() ? "(exists " : "(forall ";
			StringBuilder result = new StringBuilder(q);
			for (Local v : f.getVars()) {
				result.append("(");
				result.append(getId(v)).append(' ');
				result.append(getSort(v)).append(") ");
			}
			result.append(body).append(')');
			return result.toString();
		} finally {
			for (int i = f.getVars().size() - 1; 0 <= i; --i) {
				Local v = f.getVars().get(i);
				if (! v.equals(quantified.pop()))
					throw new IllegalStateException("Lost: " + v);
			}
		}
	}

	@Override
	public String visit(Fun f) {
		// TODO come up with a generic way to track and declare predicates
		if (f.getArgs().isEmpty())
			return f.getId();
		StringBuilder result = new StringBuilder("(");
		result.append(f.getId());
		for (Formula a : f.getArgs()) {
			result.append(' ').append(a.dispatch(this));
		}
		result.append(')');
		return result.toString();
	}

	@Override
	public String visit(IfThenElse f) {
		String cond = f.getCondition().dispatch(this);
		String thenString = f.getThenFormula().dispatch(this);
		String elseString = f.getElseFormula().dispatch(this);
		String smtFun = f.isBoolean() ? "(if_then_else " : "(ite ";
		return smtFun + cond + " " + thenString + " " + elseString + ")";
	}

	public Iterable<String> getExtraSorts() {
		if (heaps.isEmpty())
			return Collections.singleton(OBJ_TYPE);
		Set<String> result = new LinkedHashSet<String>();
		result.add(OBJ_TYPE);
		for (HeapIncarnation h : heaps) {
			result.add(h.getKey() + "Field");
		}
		return result;
	}

	public Iterable<String> getExtraPreds() {
		Set<String> result = new LinkedHashSet<String>();
		for (HeapIncarnation h : heaps) {
			String s = h.heap;
			result.add("(" + Fun.FINAL_PRED + " " + s + "Field)");
			if (heapMapEncoding && OBJ_TYPE.equals(s)) {
				Integer i = h.incarnation;
				result.add("(" + Fun.PROTECT_PRED + " " + "ObjField)");
				result.add("(" + Fun.PROTECT_PRED + i + " Obj Obj)");
			}
		}
		return result;
	}

	public Iterable<String> getExtraFuns() {
		List<String> result = new ArrayList<String>(variables.size()
				+ constants.size() + heaps.size() + arrays.size() + 1 /*null*/);

		// null
		result.add("(null " + OBJ_TYPE + ")");

		// variables
		for (Entry<String, String> v : variables.entrySet()) {
			String smtSort = v.getValue();
			result.add("(" + v.getKey() + " " + smtSort + ")");
		}

		// constants
		for (String c : constants.values())
			result.add("(" + c + " " + OBJ_TYPE + ")");

		for (HeapIncarnation h : heaps) {
			String s = h.getKey();
			Integer i = h.getValue();
			result.add("(deref" + s + i + " Obj " + s + "Field " + s + ")");
		}

		// array select and store functions
		for (HeapIncarnation a : arrays) {
			// "select<ComponentSort> Obj Int <ComponentSort>"
			// "store<ComponentSort> Obj Int <ComponentSort> Obj"
			if (useArrayStore) {
				if (0 < a.incarnation)
					throw new IllegalStateException("Shouldn't use incarnations: " + a);
				result.add("(select" + a + " Obj Int " + a.heap + ") (store" + a + " Obj Int " + a.heap + " Obj)");
			} else {
				result.add("(select" + a + " Obj Int " + a.heap + ")");
			}
		}
		return result;
	}

	public Iterable<String> getAxioms() {
		List<String> result = new LinkedList<String>();

		// array length is final
		if (variables.containsKey(Local.ARRAY_LENGTH_FIELD_NAME)) {
			result.add("(" + Fun.FINAL_PRED + " " + Local.ARRAY_LENGTH_FIELD_NAME + ")");
			for (HeapIncarnation h : heaps) {
				String s = h.getKey();
				if (! "Int".equals(s))
					continue;
				// array length always positive
				Integer i = h.getValue();
				String derefFun = "deref" + s + i;
				result.add(String.format("(forall (?a' %s) (or (= ?a' null) (<= 0 (%s ?a' %s))))",
						OBJ_TYPE, derefFun, Local.ARRAY_LENGTH_FIELD_NAME));
			}
		}

		if (useArrayStore) {
			// array axioms modeled after SMT-LIB Arrays theory
			for (HeapIncarnation a : arrays) {
				result.add(String.format("(forall (?a %s) (?i Int) (?e %s) "
						+ "(= (select%s (store%s ?a ?i ?e) ?i) ?e))",
					OBJ_TYPE, a.heap, a, a));
				result.add(String.format(
						"(forall (?a %s) (?i Int) (?j Int) (?e %s) "
								+ "(or (= ?i ?j) "
								+ "(= (select%s (store%s ?a ?i ?e) ?j) "
								+ "(select%s ?a ?j))))",
						OBJ_TYPE, a.heap, a, a, a));
			}
		}

		if (heapMapEncoding) {
			for (Map.Entry<String, IVariableBinding> f : fields.entrySet()) {
				IVariableBinding binding = f.getValue();
				if (binding == null)
					// array length
					continue;
				if (! OBJ_TYPE.equals(getSort(binding.getType())))
					// primitive field
					continue;

				RefType perm = checker.getVariableType(binding);
				if (perm == null)
					// no field permission
					continue;
				if (! perm.getPerm().isProtection())
					// permission doesn't protect against modification
					continue;

				result.add("(" + Fun.PROTECT_PRED + " " + f.getKey() + ")");

//				ITypeBinding elemType = binding.getType();
//				for (PermKind d : perm.getElemDims()) {
//					if (!elemType.isArray())
//						break;
//					elemType = elemType.getComponentType();
//					for (HeapIncarnation a : arrays) {
//						if (!a.heap.equals(getSort(elemType)))
//							continue;
//						result.add("(forall (?a Obj) (?i Int) (implies (not (= ?a null)) ()))");
//					}
//				}
			}

			for (HeapIncarnation h : heaps) {
				String s = h.getKey();
				if (! OBJ_TYPE.equals(s))
					continue;
				Integer i = h.getValue();
				result.add(String.format(
						"(forall (?o Obj) (?f ObjField) " +
							"(implies (and (not (= ?o null)) (%s ?f)) " +
								"(%s%d ?o (derefObj%d ?o ?f))))",
						Fun.PROTECT_PRED, Fun.PROTECT_PRED, i, i));
				// transitivity (may be inefficient)
				result.add(String.format(
						"(forall (?o1 Obj) (?o2 Obj) (?o3 Obj) " +
							"(implies (and (distinct ?o1 ?o2 ?o3) (%1$s%2$d ?o1 ?o2) (%1$s%2$d ?o2 ?o3)) " +
								"(%1$s%2$d ?o1 ?o3)))",
						Fun.PROTECT_PRED, i));

				// protect array field contents
//				for (Map.Entry<String, IVariableBinding> f : fields.entrySet()) {
//					IVariableBinding binding = f.getValue();
//					ITypeBinding type = binding.getType();
//					if (!type.isArray())
//						continue;
//
//					RefType perm = checker.getVariableType(binding);
//					if (perm == null)
//						// no field permission
//						continue;
//					if (! perm.getPerm().isProtection())
//						// permission doesn't protect against modification
//						continue;
//					if (perm.getElemDims().length <= 0)
//						// no array dimension permissions
//						continue;
//
//					String elemSort = getSort(type.getComponentType());
//					for (HeapIncarnation a : arrays) {
//						if (!a.heap.equals(elemSort))
//							continue;
//						result.add("(forall (?o Obj) (?a Obj) (?i Int) (implies (and (not (= ?a null)) (= ?a (derefObj0 ?o f.getKey()))) (protect0 ?a (select + a ?a ?i))))");
//					}
//				}
			}
		}

		// disjoint fields axioms
		Map<String, String> disjoint = new LinkedHashMap<String, String>();
		for (Map.Entry<String, String> v : variables.entrySet()) {
			if (v.getValue().endsWith("Field")) {
				String list = disjoint.get(v.getValue());
				if (list == null)
					list = v.getKey();
				else
					list = list + " " + v.getKey();
				disjoint.put(v.getValue(), list);
			}
		}
		for (String list : disjoint.values()) {
			if (! list.contains(" "))
				// only one variable in this list
				continue;
			result.add("(distinct " + list + ")");
		}
		return result;
	}

	private String getSort(Local l) {
		String result = getSort(l.getType());
		if (Local.FIELD_META_TYPE.equals(l.getMetaType()))
			result = result + "Field";
		return result;
	}

	/**
	 * Maps from Java types to SMT sorts
	 * @param type can be {@code null} for the type of {@code null} expressions.
	 * @return SMT sort used for representing the given type
	 */
	private String getSort(ITypeBinding type) {
		String javaType = type == null ? "null" : type.getName();
		String smtType;
		if ("boolean".equals(javaType))
			smtType = "Bool";
		else if ("int".equals(javaType) || "long".equals(javaType) || "byte".equals(javaType) || "short".equals(javaType))
			smtType = "Int";
		else if ("float".equals(javaType) || "double".equals(javaType))
			smtType = "Real";
		else // this includes arrays
			smtType = OBJ_TYPE;
		return smtType;
	}

	private static class HeapIncarnation implements Map.Entry<String, Integer> {

		private final String heap;
		private final Integer incarnation;

		public HeapIncarnation(String heap, int incarnation) {
			super();
			this.heap = heap;
			this.incarnation = incarnation;
		}

		@Override
		public String getKey() {
			return heap;
		}

		@Override
		public Integer getValue() {
			return incarnation;
		}

		@Override
		public Integer setValue(Integer value) {
			throw new UnsupportedOperationException();
		}

		@Override
		public String toString() {
			return heap + incarnation;
		}

		@Override
		public int hashCode() {
			final int prime = 31;
			int result = 1;
			result = prime * result + ((heap == null) ? 0 : heap.hashCode());
			result = prime * result
					+ ((incarnation == null) ? 0 : incarnation.hashCode());
			return result;
		}

		@Override
		public boolean equals(Object obj) {
			if (this == obj)
				return true;
			if (obj == null)
				return false;
			if (getClass() != obj.getClass())
				return false;
			HeapIncarnation other = (HeapIncarnation) obj;
			if (heap == null) {
				if (other.heap != null)
					return false;
			} else if (!heap.equals(other.heap))
				return false;
			if (incarnation == null) {
				if (other.incarnation != null)
					return false;
			} else if (!incarnation.equals(other.incarnation))
				return false;
			return true;
		}

	}
}
